Nuprl Lemma : cr-explanation-step 13,45

es:ES, Cmd:Type, In:AbsInterface(Cmd), Sys:AbsInterface(Top).
(E(Inr E(Sys))
 (f:sys-antecedent(es;Sys).
 (u:E(Sys). (f(u) = u  E)  ((u  In)))
  (e:E(Sys).
  cr-explanation{i:l}
  cr-explanation(esSysfe)
  =
  cr-explanation{i:l}
  cr-explanation(esSysf; (f(e)))
   (E(In) List))) 
latex


Upabstract chain replication
Definitionss = t, t  T, x:AB(x), x:AB(x), EState(T), a:A fp B(a), f(a), Id, , strong-subtype(A;B), P  Q, Type, EqDecider(T), Unit, left + right, IdLnk, x:A  B(x), EOrderAxioms(Epred?info), kindcase(ka.f(a); l,t.g(l;t) ), Knd, loc(e), kind(e), Msg(M), type List, , val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), r  s, e < e', , b, constant_function(f;A;B), SWellFounded(R(x;y)), , pred!(e;e'), x,yt(x;y), <ab>, A, pred(e), first(e), xt(x), P & Q, Top, ES, AbsInterface(A), E(X), E, e c e', {x:AB(x)} , ff, sys-antecedent(es;Sys), inr x , tt, inl x , case b of inl(x) => s(x) | inr(y) => t(y), True, False, e  X, let x,y = A in B(x;y), t.1, if b then t else f fi , cr-explanation{i:l}(esSysfe), x  dom(f), (x  l), f**(e), es-prior-fixedpoints{i:l}(esSysfe), P  Q, (e < e'), P  Q, P  Q, f(x)?z, S  T, T, s ~ t, x.A(x), Dec(P), x:AB(x), e<e'.P(e), ee'.P(e), e<e'P(e), ee'.P(e), e[e1,e2).P(e), e[e1,e2).P(e), e[e1,e2].P(e), e[e1,e2].P(e), e(e1,e2].P(e), SqStable(P), a =!x:TQ(x), InvFuns(A;B;f;g), Inj(A;B;f), IsEqFun(T;eq), Refl(T;x,y.E(x;y)), Sym(T;x,y.E(x;y)), Trans(T;x,y.E(x;y)), AntiSym(T;x,y.R(x;y)), Connex(T;x,y.R(x;y)), CoPrime(a,b), Ident(T;op;id), Assoc(T;op), Comm(T;op), Inverse(T;op;id;inv), BiLinear(T;pl;tm), IsBilinear(A;B;C;+a;+b;+c;f), IsAction(A;x;e;S;f), Dist1op2opLR(A;1op;2op), fun_thru_1op(A;B;opa;opb;f), FunThru2op(A;B;opa;opb;f), Cancel(T;S;op), monot(T;x,y.R(x;y);f), IsMonoid(T;op;id), IsGroup(T;op;id;inv), IsMonHom{M1,M2}(f), a  b, IsIntegDom(r), IsPrimeIdeal(R;P), f  g, X(e), sender(e), e loc e' , (e <loc e')
Lemmasiff wf, rev implies wf, es-fix-step, es-le-causle, es-fix wf, strong-subtype-set3, strong-subtype wf, strong-subtype-self, es-fix wf2, sq stable all, sq stable from decidable, decidable es-causle, es-causl wf, es-prior-fixedpoints-fix, es-prior-fixedpoints wf, squash wf, event system wf, sys-antecedent wf, es-E-interface-subtype rel, true wf, btrue wf, bfalse wf, es-causle wf, es-E wf, es-interface wf, es-E-interface wf, deq wf, EOrderAxioms wf, IdLnk wf, Msg wf, unit wf, nat wf, val-axiom wf, qle wf, cless wf, bool wf, top wf, Knd wf, kindcase wf, constant function wf, assert wf, not wf, loc wf, pred! wf, strongwellfounded wf, member wf, rationals wf, Id wf, EState wf, subtype rel wf

origin